\begin{tabbing}
$\forall$\=$E$:Type, ${\it pred?}$:($E$$\rightarrow$($E$+Unit)), ${\it info}$:($E$$\rightarrow$(Id$\times$Id+(IdLnk$\times$$E$)$\times$Id)), $V$:(Id$\rightarrow$Id$\rightarrow$Type),\+
\\[0ex]$M$:(IdLnk$\rightarrow$Id$\rightarrow$Type), $T$:(Id$\rightarrow$Id$\rightarrow$Type), ${\it init}$:($i$,$x$:Id$\rightarrow$$T$($i$,$x$)),
\\[0ex]${\it Trans}$:($i$:Id$\rightarrow$$k$:Knd$\rightarrow$kindcase($k$; $a$.$V$($i$,$a$); $l$,$t$.$M$($l$,$t$) )$\rightarrow$($x$:Id$\rightarrow$$T$($i$,$x$))$\rightarrow$($x$:Id$\rightarrow$$T$($i$,$x$))),
\\[0ex]${\it Choose}$:($i$,$a$:Id$\rightarrow$($x$:Id$\rightarrow$$T$($i$,$x$))$\rightarrow$($V$($i$,$a$)+Unit)),
\\[0ex]${\it Send}$:($i$:Id$\rightarrow$$k$:Knd$\rightarrow$kindcase($k$; $a$.$V$($i$,$a$); $l$,$t$.$M$($l$,$t$) )$\rightarrow$($x$:Id$\rightarrow$$T$($i$,$x$))$\rightarrow$(Msg($M$) List)),
\\[0ex]${\it val}$:($e$:$E$$\rightarrow$kindcase(kind($e$); $a$.$V$(loc($e$),$a$); $l$,$t$.$M$($l$,$t$) )).
\-\\[0ex]($\forall$$e$:$E$. $\neg$first($e$) $\Rightarrow$ loc(pred($e$)) $=$ loc($e$) $\in$ Id)
\\[0ex]$\Rightarrow$ SWellFounded(pred!($e$;${\it e'}$))
\\[0ex]$\Rightarrow$ val{-}axiom($E$;$V$;$M$;${\it info}$;${\it pred?}$;${\it init}$;${\it Trans}$;${\it Choose}$;${\it Send}$;${\it val}$) $\in$ Prop
\end{tabbing}